By way of general background, scripting languages are programming languages that control software systems, applications and programs. Scripts are often treated as distinct from “programs,” which execute independently from other applications. In addition, scripts can be distinct from the “core code” of an application, which may be written in a different language. Scripts can be written by developers or other programs, in source formats or object formats, which range the gamut in terms of human friendly or machine friendly, or neither. Where accessible to the end user, scripts enable the behavior of an application to be adapted to the user's needs. Scripts can also be interpreted from source code or “semi-compiled” to bytecode, or another machine friendly format, which is interpreted. Scripting languages can also be embedded in an application with which they are associated.
For further background, a type system defines how a programming language classifies values and expressions into types, how it can manipulate those types and how they interact. A type identifies a value or set of values as having a particular meaning or purpose, although some types, such as abstract types and function types, might not be represented as values in the executing program. Type systems vary significantly between languages, e.g., among other kinds of differences, type systems can vary with their compile-time syntactic and run-time operational implementations.
For an example of how types can be used, a compiler can use the static type of a value to optimize storage and the choice of algorithms for operations on the value. In many C compilers, for example, the nominally typed “float” data type is represented in 32 bits in accordance with an accepted norm for single-precision floating point numbers. C thus uses floating-point-specific operations on those values, e.g., floating-point addition, multiplication, etc. In addition, the depth of type constraints and the manner of their evaluation can have an effect on the typing of the language.
An efficient, logical and expressive type system is desirable to keep language compact, but also highly expressive and logical so that efficient and structurally compact data intensive applications can be generated along with efficient storage representations. However, type systems of conventional programming languages are not general enough or flexible enough for the complexities of massive scale data processing and consumption. In short, any complexity or lack of flexibility of a type system and associated inefficiency can magnify exponentially or out of proportion when large amounts of data are implicated. For the same reasons, the type checking processes that determine whether or not types have been validly specified in programming code have the same limitations of the type systems to which they apply.
In this regard, the ability to express types richly and efficiently, given the diversity of data values in the computing universe, can significantly improve the resulting performance of data intensive applications and programs. A need thus remains for a programming language with an improved type system, along with a way to check that types of the programming language are valid prior to execution with errors. Accordingly, algorithms are desired for type-checking programs in a data scripting language with an expressive type system.
More specifically, the ability to determine the validity of subtype relationships where a programming construct includes a statement that a first type is a subtype of a second type is of particular help for a type system supporting type test and refinement if programs are to be statically verified.
In this regard, a typechecking algorithm often needs to test whether one type S is a subtype of another type T, meaning that any value of the subtype S may be used in a place where the supertype T is expected. A conventional approach is to define a set of syntactic rules for testing subtyping between S and T, i.e., use a subtype algorithm based on the syntax of types. However, this approach is problematic in the context of refinement types, because it is complicated to reflect refinement constraints, which may include logical connectives, such as and, or, negation, and equations as syntactic rules.
One conventional system proposes using a theorem prover to implement semantic subtyping. Such system uses the theorem prover for a propositional spatial logic whose logical connectives are: not, and, zero, composition, guarantee, location, placement, name equality, but with no quantifiers and where the only terms are names. However, this is by no means standard logic, the particular algorithm presented does not scale well and is thus of limited use in practice. There are also some conventional typecheckers that make use of an automated theorem prover during typechecking to check the constraints associated with refinement types, however, again such systems use conventional syntactic rules to determine subtyping, as opposed to using semantic subtyping.
The above-described background information and deficiencies of current type systems and corresponding subtype checking of programming languages are merely intended to provide a general overview of some of the background information and problems of conventional systems, and are not intended to be exhaustive. Other problems with conventional systems and corresponding benefits of the various non-limiting embodiments described herein may become further apparent upon review of the following description.